$\forall$$A$:Type, $P$:($A$$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$). ($\forall$$x$:$A$. Dec($\exists$$n$:$\mathbb{N}$. ($\uparrow$($P$($x$,$n$))))) $\Rightarrow$ ($\forall$$x$:$A$. $\exists$$y$:$\mathbb{N}$ + Top. p{-}mu($P$($x$);$y$))